可满足性模块理论(SMT)基础

2023-08-15 22:02| 来源: 网络整理| 查看: 265

可满足性模块理论(SMT)基础 - 01 - 自动机和斯皮尔伯格算术前言

如果，我们只给出一个数学问题的（比如一道数独题）约束条件，是否有程序可以自动求出一个解？可满足性模理论(SMT - Satisfiability Modulo Theories)已经可以实现这个需求。

因此，最近想搞明白z3的实现原理。源代码没有读两句，还是找了本教材来看。 Vijay Ganesh (PhD. Thesis 2007), Decision Procedures for Bit-Vectors, Arrays and Integers 现在的任务是：

看懂这本书，搞清楚求解逻辑。再搞清楚，如何使用SMT来求解各种问题？可满足性模理论(SMT - Satisfiability Modulo Theories) 基本概念

数学上，这个问题属于逻辑的范畴。

一阶逻辑(First-Order Logic)及其语法

一阶逻辑: 逻辑函数的参数可以是变量，但是不能是函数。书中把一阶逻辑看成一种数学语言。这种语言的语法(Syntax)由字母系统(Alphabet)和构造法则(formation rules)组成。

字母系统(Alphabet)

包括逻辑符号和非逻辑符号。

Logical Symbols Parentheses: (, ) Quantifier: \(\forall\)(for all), \(\exists\)(there exists) Boolean Connectives: \(\lnot\)(not), \(\land\)(and), \(\lor\)(or) Constant formulas: true, false Equality: = Non-logical Symbols Variables: usually represented by letters x, y, z... Function Symbols: 函数符号通常使用小写字母来表示，f, g, h,... 函数符号的返回类型一般不是Boolean类型。比如：f(x)可以表示为"x的父亲"。 Relation Symbols(关系符号) or predicate symbols(谓词符号): Each relation symbol also has an associated arity 谓词符号一般使用大写字母来表示，P, Q, R, ... 谓词符号代表一个返回值为Boolean类型的函数。比如：P(x)可以表示"x是否是一个人"。构造法则(Formation Rules)

包括术语(terms)和公式(formulas)。

术语(terms) 包括变量(variables)和函数(functions)。公式(formulas) 包括：谓词符号，等式(equality)，逻辑运算符号(\(\lnot, \land, \lor\)), 修饰符(quantifiers) 其它概念原子公式(atomic formula) 由谓词符号和等式组成的公式。原子公式不包含逻辑运算符号和修饰符。文字(literals) 包括：原子公式和其否定。无修饰公式(quantifier-free formulas) 由谓词符号、等式和逻辑运算符号组成的公式。比如： \(p(x)\)。量化公式(quantified formulas) 带修饰符号的公式。比如： \(\forall x p(x)\)。自由变量(free variable) 比如： \(p(x)\)中的\(x\)。界限变量(bound variables) 量化公式中被限定的变化。比如： \(\forall x p(x)\)中的\(x\)。一阶逻辑的理论和模型

这里说的理论是一个需要求解的推测.

理论(theories) 一个理论是一套一阶命题(sentence),这些命题,在一套公理(axioms)的基础上,是可以被推理出来的. 我们的目的是求解出命题中变量的值,以满足所有的命题.

模型(model) 模式是一个满足一个给定理论(所有命题)的一阶结构,表示为\(dom(M)\). \(\phi\)是一个赋值方法,给\(\theta(\bar{x})\)的每个变量赋值一个M的元素. \(M \models_\rho \theta(\bar{x})\)表示\(M\)和\(\phi\)满足(satisfy)\(\theta(\bar{x})\).

Theory -> signature(\(\Sigma\)) -> dom(m)

稳固性(soundness) 论证的每一步在数学上都是正确的。如果返回值为"不可满足(unsatisfiable)"，则确实是不可满足。

完备性(completeness) 如果返回值为“可满足”，则确实为可满足。并可以生成用于得出结论的所有事实。

在线(online) 决策程序以一种递增的方式接受处理新的输入，而不需要重新处理之前已经处理过的输入。

证明生成(proof-producing) 指决策程序可以对处理过程产生一个数学证明。

SAT(boolean satisfiability problem) - 布尔可满足性问题给定一个逻辑公式，判断是否存在解。

现有的各种方法皮尔斯伯格算术(Presburger arithmetic) 皮尔斯伯格算术公式的定义

\[f \equiv a^T \cdot x \sim c \text{, atomic formulas} \\ f ::= \lnot f_1 | f_1 \land f_2 | f_1 \lor f_2 \\ where \\ a \text{: a column vector of integer constants} \\ c \text{: an integer constants} \\ x \text{: a column vector of integer variables} \\ a^T \text{: a row vector} \\ \sim \text{: an operator from } \{=, \ne, , \ge\} \\ \]

解决方案(solution)的数学表达

一个_解决方案_是一个使得公式\(\phi\)为true的变量赋值w。 \(Sol(\phi)\)为公式\(\phi\)所有的解决方案。

注：\(\phi\)应该就是皮尔斯伯格算术定义的公式。下面是解决方案\(Sol(\phi)\)的递归定义：

\[if \ \phi \text{ is atomic, then } Sol(\phi) = \{ w \in \mathbb{Z^n} | a^T \cdot w \sim c \} \\ if \ \phi \equiv \lnot \phi_1 \text{, then } Sol(\phi) = \mathbb{Z}^n - Sol(\phi1_1) \\ if \ \phi \equiv \phi_1 \land \phi_2 \text{, then } Sol(\phi) = Sol(\phi1_1) \cap Sol(\phi1_2) \\ if \ \phi \equiv \phi_1 \lor \phi_2 \text{, then } Sol(\phi) = Sol(\phi1_1) \cup Sol(\phi1_2) \\ where \\ \mathbb{Z} \text{: the set of integers} \\ w \text{: n-vector of integers} \\ \mathbb{Z^n} \text{: n integers} \\ \]

\(\{ a | b \}\)为满足\(b\)条件下的\(a\)。

自动化的思路确定性有限状态自动机DFA(deterministic finite-state automaton) \(A_{\phi}\) 一个解决方案w的数学表达

\[w = \begin{Bmatrix} w_1 \\ \cdots \\ w_n \end{Bmatrix} \\ = \begin{Bmatrix} b_{10} & \cdots & b_{1m} \\ \cdots & \cdots & \cdots \\ b_{n0} & \cdots & b_{nm} \\ \end{Bmatrix} \text{, binary matrix} \\ = \begin{Bmatrix} b_{10} \cdots b_{1m} \\ \cdots \\ b_{n0} \cdots b_{nm} \\ \end{Bmatrix} \text{, a vector binary strings} \\ = \begin{Bmatrix} b_{0} & \cdots & b_{m} \\ \end{Bmatrix} \text{, a vector of languages} \\ where \\ w_x = \begin{Bmatrix} b_{x0} & \cdots & b_{xi} \\ \end{Bmatrix} \text{, 2's complement form, } b_{x0} \text{: sign bit} \\ b_{xy} \in \mathbb{B} \\ \mathbb{B} = \{0, 1 \} \\ b_x = \begin{Bmatrix} b_{1x} \\ \cdots \\ b_{nx} \\ \end{Bmatrix} , \ b_x \text{ is denoted as a letter}\\ \]

2补数(2's complement) 一种使用2进制表示有符号数的方法。第一位为符号位，如果是0，则记做0; 如果为1，则记做\(-2^{n-1} \text{, n is the size of the number}\)。例如： 0010为2; 1010为-6。

语言\(L_f\) 是公式f的所有解决方案形成的所有字符串的集合。

自动机的正式描述

自动机\(A_f\)可以理解为一个类的实例，属性： formula state 方法： read(), transition(), satisfied() output() 无限自动机\(A_f\)的数学描述：

\[A_f = (S, \mathbb{B}^n, \delta, s_{initial}, S_{acc}) \\ where \\ S = \mathbb{Z} \cup \{ s_{initial} \} \text{ is the set of states, } \mathbb{Z} \text{ is the set of integers and } s_{initial} \notin \mathbb{Z} \\ s_{initial} \text{ is the start state} \\ \mathbb{B}^n \text{ is the alphabet, which is the set of n-bit vectors, } \mathbb{B} = \{0, 1\} \\ \text{The transition function } \delta : S \times \mathbb{B}^n \to S \text{ is defined as follows:} \\ \quad \delta(s_{initial}, b) = -a^T \cdot b \\ \quad \delta(l, b) = 2l + a^T \cdot b \\ \quad where \ l \in \mathbb{Z} \text{ is a non-initial state} \\ S_{acc} \text{: the set of accepting states}: S_{acc} = \{ l \in \mathbb{Z} | l \sim c \} \cup \begin{cases} \{ s_{initial} \} & if \ a^T \cdot 0 \sim c \\ \emptyset & otherwise \end{cases} \]

自动机的状态 \(l\)是自动机\(A_f\)的状态。

\[l_{initial} = -a^T \cdot b_0 \text{, since } b_0 \text{ are sign bits} \\ l_{x+1} = a^T \cdot \begin{Bmatrix} b_{10} & \cdots & b_{1x+1} \\ \cdots & \cdots & \cdots \\ b_{n0} & \cdots & b_{nx+1} \\ \end{Bmatrix} \\ \ \ = 2l_x + a^T \cdot b_{x+1} \]

自动机的接受条件 \(l \sim c\)

自动机的结果当满足接受条件时，\(b\)的值。

为什么是无限的？

这里说的无限是指状态\(l\)的可能性。基本上存在于所有的整数\(\mathbb{Z}\)中了。

转变为有限自动机，需要的过程。

2个定义: 对系数\(a^T = (a_1, \cdots, a_n)\)：

\[\lVert a^T \rVert_{-} = \sum_{\{i | a_i < 0\}} \vert a_i \vert \\ \lVert a^T \rVert_{+} = \sum_{\{i | a_i > 0\}} \vert a_i \vert \]

推论：

\[-a^T \cdot b = \lVert a^T \rVert_{-} - \lVert a^T \rVert_{+} \leq \lVert a^T \rVert_{-} \\ a^T \cdot b = \lVert a^T \rVert_{+} - \lVert a^T \rVert_{-} \leq \lVert a^T \rVert_{+} \]

引理1：给定一个原子的皮尔斯伯格算术公式\(a^T \cdot x \sim c\), a对应的自动机\(A_f\)，a当前这个自动机的状态\(l \in \mathbb{Z}\)，有下面断言：

如果\(l > \lVert a^T \rVert_{-}\), 则下一个状态\(l'\)，有\(l' > l\)。如果\(l < \lVert a^T \rVert_{+}\), 则下一个状态\(l'\)，有\(l' < l\)。

根据引理，自动机的状态的可能性为：

\[S = [\min(-\lVert a^T \rVert_{+}, c), max(\lVert a^T \rVert_{-}, c)] \cup \{ s_{initial}, s_{-\infty}, s_{+\infty} \} \]

这就可以变成有限自动机。

有限自动机的正式描述

有限自动机\(A_f\)的数学描述：

\[A_f = (S, \mathbb{B}^n, \delta, s_{initial}, S_{acc}) \\ where \\ S = [\min(-\lVert a^T \rVert_{+}, c), max(\lVert a^T \rVert_{-}, c)] \cup \{ s_{initial}, s_{-\infty}, s_{+\infty} \} \\ s_{initial} \notin \mathbb{Z} \\ s_{initial} \text{ is the start state} \\ \mathbb{B}^n \text{ is the alphabet, which is the set of n-bit vectors, } \mathbb{B} = \{0, 1\} \\ \text{The transition function } \delta : S \times \mathbb{B}^n \to S \text{ is defined as follows:} \\ \quad \delta(s_{initial}, b) = -a^T \cdot b \\ \quad \delta(s_{+\infty}, b) = s_{+\infty} \\ \quad \delta(s_{-\infty}, b) = s_{-\infty} \\ \quad \delta(l, b) = \begin{cases} s_{+\infty} & if \ 2l + a^T \cdot b > max(\lVert a^T \rVert_{-}, c) \\ s_{-\infty} & if \ 2l + a^T \cdot b > max(-\lVert a^T \rVert_{+}, c) \\ 2l + a^T \cdot b & otherwise \\ \end{cases} \\ S_{acc} \text{: the set of accepting states}: \\ S_{acc} = \{ l \in \mathbb{Z} | l \sim c \} \\ \quad \cup \\ \begin{cases} \{ s_{initial} \} & if \ a^T \cdot 0 \sim c \\ s_{+\infty} & if \ \sim \in \{ >, \geq, \neq \} \\ s_{-\infty} & if \ \sim \in \{

【本文地址】

公司简介

联系我们